Elephant logic

The axioms are such that all results of inference include their history.
The simplest kind of axiom that works for this is

b(p,r1) ∧ b(p imp q,r2) ⊃ b(q,mp(p,q,r1,r2)).

However, this doesn't contain enough information about the state
of the database to do non-monotonic reasoning.  For this we need
the database as a parameter and axioms that describe how it changes.

holds(p,r1,db) ∧ holds(p imp q,r2,db) ⊃ holds(q,mp(p,q,r1,r2),result(mp(p,q,r1,r2),db))

We also require

holds(p,r,db) ⊃ holds(p,r,result(mp(x,y,z,w),db))

which expresses the monotonicity of modus ponens.

In order to get an example of non-monotonicity, it seems easiest to
take an example from default logic.

rule(name(p,Mq,r),db) ∧ holds(p,r1,db) ∧ consistent(q,db) ⊃
	holds(r,default(name,p,q,r),r1),result(default(name(p,q,r),r1),db))

Of course, this gives no opportunity to infer new rules.  I suppose this
still preserves all information in the database, but it mightn't preserve
something like

follows(p,db)

if non-monotonic rules were involved in the derivation of  p,
which the preceding axiom would.  Thus we have

follows(q,db) ⊃ follows(q,result(mp(x,y,z,w),db)).

The next tasks seem to be:

1. Formalize all prop-calc in one go, i.e. with predicate prop-calc.

2. Look at reasoning involving variables.

3. Do a heuristic.

4. Do the predicates that permit expressing a preference for
the acceptance of results early in the reasoning.  This is the
main goal of elephant-logic.

Maybe we need a name that doesn't confuse people into thinking
it's a new form of logic.  Perhaps an elephant metatheory of
first order logic.

We need to be able to say, "What we know about Y is derived from
what we know about X".  We also need  abnormality(X).  Then we can
say

derived(Y,X) ⊃ prefer(abnormality(Y),abnormality(X)).

****
October 9 (Timothy is 23 months)

Perhaps we don't need to derive the history explicitly in the axioms.
Instead we can refer to the history as a function of the wff and the
database.
Actually let's consider  P  to be an occurrence of a formula  p  rather than
the abstract formula itself.  It's the occcurrences that have histories
rather than the formulas themselves.

We have

wff(P)

and

occurrences(p,s)

which may be  nil.


We have the predicate

observation(P,s)

which is true if  P  entered the database  s  by observation.

We also have

from-mp(P,s)

if  P  entered  s  by a modus ponens.

In that case the functions  major(P,s)  and  minor(P,s)  are defined
as the occurrences of the major and minor premisses of  P.

We now have

result(modus(P1,P2),s)

which is the database that results from performing a modus ponens with
premisses  P1  and  P2.  Very likely we want to require that when
P1 and P2 do not admit a modus ponens, then

result(modus(P1,P2),s) = s.

Perhaps it is useful to allow formulas like EKL proof checker commands.
For example, we can have

result(derive(p,U),s).

This is the database that results from attempting to derive the wff p
from the set U of occurrences of wffs in the database s.  If the
derivation of p from U is successful, then result(derive(p,U),s) is s
extended by a new occurrence of p.  On the other hand, if the action
derive(p,U)  is unsuccessful, then result(derive(p,U),s)
is  s  extended by an occurrence of

not derivable(p,U,s).

We will need names for sets of occurrences that include at least
explicit listing and also the whole database.  We may also need
variants with different concepts of derivation.

This statement can be used as a premiss in non-monotonic rules.  However,
there is a small complication.  The system may have reached the conclusion that
something was not derivable several steps previous to the time it wants to
be used.  It's still ok to use it, provided all the reasoning in between
was monotonic, i.e. what was proved several steps previously still holds
and is an adequate premiss.  This means that the rules of inference must
allow reference to such previously shown database referential statements.
But this is just the kind of elephantine property that should be expected.

	Rewrite commands as in EKL should also be useful.

	Do we need the formula

latest(s)

for the latest formula in a database?  If we have it, we can write

P1 ε s ∧ P2 ε s ∧ ok-mp(wff(P1),wff(P2)) ⊃ from-mp(latest(result(modus(P1,P2),s)))

and similar axioms.

Sentences about the database itself. WE UPSTAGED THIS POINT.

To avoid paradox we should not have sentences about  s  within  s,
but there is nothing to prevent there being sentences about the
predecessors of  s.  If we assume that formulas are added to  s
successively, then the function

pred(s)

is defined and gives the preceding database.

We can have queries about a database, but these give rise to
new databases.  Consider for example

result(query p,s).

We will have either

occurs(in(p,s),result(query p,s))

or

occurs(not in(p,s),result(query p,s)).

More complex queries can be made, e.g. whether a certain wff
is a consequence of the database.  The result of such a query
can be entered in the next database or it can merely serve
as the premiss of some deduction.

Question: Do the logical operations combine wffs or occurrences
of wffs?  Do we have  p and q  or  P and Q?  The latter is
more powerful in terms of the ability to express heuristics,
but may not be necessary.

Maybe the next problem is to see what we need to express a heuristic.

Goals

	We want to treat goals and generated subgoals.  Is there
anything wrong with having

occurs(goal p,s)

in the database?

	Consider the action  assume(p)  leading to the database

result(assume p,s).

	We allow it, but the pedigree of the resulting occurrence
of  p  includes the fact that it is an assumption.  It suggests
also having the function

assumptions(P,s)

giving the assumptions used in deriving the wff-occurrence  P.
We will abbreviate "wff-occurrence" by "wffo".  We clearly
need an analog of the natural deduction rule ⊃i that discharges
assumptions.

1987 Oct 30

Maybe we don't need so many mental situations.  We surely need
a new one whenever we observe the present situation and reach
a non-monotonic conclusion about it.